/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.api;

import java.io.StringReader;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Expr;
import alloy.ast.FindCommand;
import alloy.ast.IntExprCastExpr;
import alloy.ast.Location;
import alloy.ast.ModuleInfo;
import alloy.ast.SigmaExpr;
import alloy.bool.PartialAssignment;
import alloy.parse.AlloyParser;
import alloy.parse.AlloyPrepass;
import alloy.parse.ParseException;
import alloy.parse.visitor.MakeASTVisitor;
import alloy.semantic.CheckHigherOrderQuantifiersVisitor;
import alloy.semantic.ExprTypeCheckVisitor;
import alloy.semantic.LocalScope;
import alloy.semantic.NoParagraphNameShadowingVisitor;
import alloy.transform.DesugarDeclsVisitor;
import alloy.transform.DesugarIntExprCastExprVisitor;
import alloy.transform.DesugarLetVisitor;
import alloy.transform.DesugarMultFormulasVisitor;
import alloy.transform.DesugarOverrideVisitor;
import alloy.transform.DesugarQuantifiersVisitor;
import alloy.transform.DesugarRestrictionVisitor;
import alloy.transform.DesugarSumExprVisitor;
import alloy.transform.IntCastRemovalVisitor;
import alloy.transform.InvocationInlineVisitor;
import alloy.transform.SimplifyVisitor;
import alloy.transform.atomize.AtomizationState;
import alloy.transform.atomize.AtomizationVisitor;
import alloy.transl.ASTInfoVisitor;
import alloy.transl.ExprTransl;
import alloy.transl.Transl;
import alloy.transl.TranslVisitor;
import alloy.transl.TranslatableASTCheckVisitor;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.util.Dbg;
import alloy.util.Msg;
import alloy.util.Params;
import alloy.viz.alloyviz.AlloyAtom;
import alloy.viz.alloyviz.AlloyRelation;
import alloy.viz.alloyviz.AlloySet;
import alloy.viz.alloyviz.AlloyTuple;
import alloy.viz.alloyviz.AlloyType;
import alloy.viz.alloyviz.CustVar;
import alloy.viz.alloyviz.CustVarHandler;

/**
 * Evaluates arbitrary Alloy expressions given a model solution
 **/

public class AlloyEvaluator implements Dbg.DbgMsgListener {

    private static final String[] METHODS = { "Expression", "Formula", "IntExpression" };
    private static final int EXPR = 0;
    private static final int FORMULA = 1;
    private static final int INT_EXPR = 2;
    private static final int NUM_METHODS = 3;
    private static final String NO_FILE_INFO = " " + Location.NOT_FROM_FILE + ",";
    
    private String _syntaxErr;
    private String _semanticErr;
    private final SolutionData _sol;
    private final AtomizationVisitor _atomVisitor;

    /**
     * @param spec_ model specification
     * @param fs_ FunctionSkolemizer object used to skolemize functions in <code>spec_</code>
     * @param sol_ SolutionData object obtained by analyzing a command in <code>spec_</code>
     **/
    public AlloyEvaluator(SolutionData sol_) {

        _sol = sol_;
        _syntaxErr = "";
        _semanticErr = "";
        if (sol_ != null) {
            _atomVisitor = new AtomizationVisitor(((FindCommand)sol_.getCommand()));
            //_atomVisitor.setupAtomizationVisitor();
        } else {
        	_atomVisitor = null;
        }
        Dbg.addDbgMsgListener(Dbg.USER, this);
    }

    /** @see alloy.api.AlloyRunner._performSemanticChecks */
    private alloy.ast.Node _performSemanticChecks(alloy.ast.Node astNode) {

        ModuleInfo currentInfo = _sol.getSpecification().getFocus().getModuleInfo();

        // NoParagraphNameShadowingVisitor
        astNode.applyVisitor(new NoParagraphNameShadowingVisitor(currentInfo));
        if (Dbg.userError)
            return astNode;


        try {
            // ExprTypeCheckVisitor
            astNode =
                ExprTypeCheckVisitor.typecheckNode(
                    astNode,
                    currentInfo,
                    new LocalScope(),
		    _sol.getTranslator().getCommand().skolemTypes);
        } catch (ExprTypeCheckVisitor.TypeCheckException tce) {
        }

        return astNode;
    }

    /** @see alloy.api.AlloyRunner._performElaborations */
    private alloy.ast.Node _performElaborations(alloy.ast.Node astNode) {
	
        // InvocationInlineVisitor
        astNode =
            (alloy.ast.Node)astNode.applyReturnVisitor(
                    new InvocationInlineVisitor(_sol.getSkolemizer(),
                    _sol.getSpecification().getFocus().getModuleInfo()));
        
        // see alloy.api.AlloyRunner._performElaborations
    	astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarLetVisitor());
            // DesugarOverrideVisitor
            astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarOverrideVisitor());
    	    //System.out.println("____________DesugarRestrictionVisitor____________");
    	astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarRestrictionVisitor());

    	//System.out.println("____________DesugarSumExprVisitor____________");
    	astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarSumExprVisitor());

        if (Dbg.userError)
            return astNode;
	
        // IntCastRemovalVisitor
        astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new IntCastRemovalVisitor());
        
        astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarIntExprCastExprVisitor());        

        // see alloy.transform.GenCommandFormulasVisitor.__applyOptimizationsAndDesugar
//      desugar multiplicity formulas
        astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarMultFormulasVisitor());
        //System.out.println(astNode.pp());
        // desugar quantifiers
        astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarQuantifiersVisitor());
        // desugar declarations
        astNode.applyVisitor(new DesugarDeclsVisitor());
        // desugar quantifiers generated in declaration constraints
        astNode = (alloy.ast.Node)astNode.applyReturnVisitor(new DesugarQuantifiersVisitor());
        // simplify
        astNode.applyVisitor(new SimplifyVisitor());
        // set leaf IDs
	//System.out.println("cmd=" + _sol.getCommand());
	//System.out.println("sliv=" + _sol.getCommand().sliv);
	//System.out.println("skolemMap=" + _sol.getCommand().skolemMap);
	alloy.transform.LeafIdMap oldMap = _sol.getCommand().sliv.getSkolemLeafIdMap();
	_sol.getCommand().sliv.setSkolemLeafIdMap(_sol.getCommand().skolemMap);
        astNode.applyVisitor(_sol.getCommand().sliv);
	_sol.getCommand().sliv.setSkolemLeafIdMap(oldMap);
        // no higher-order quantifiers
        if (!Params.glob.getBoolParam("MAIN", "allowhigherorder")) {
            astNode.applyVisitor(new CheckHigherOrderQuantifiersVisitor());
        }

        // atomization!
        try {
            astNode = (alloy.ast.Node)astNode.applyReturnVisitor(_atomVisitor);
            astNode.applyVisitor( AtomizationState.getFLIV(((FindCommand)_sol.getCommand())));
        } catch (Exception e) {
            e.printStackTrace();
            Dbg.fatal("atomization problem in evaluator ", e);
        }

        // sanity check . . .

        if (!(astNode instanceof SigmaExpr)) {
            astNode.applyVisitor(new TranslatableASTCheckVisitor());
        } else {
            for (Iterator terms = ((SigmaExpr)astNode).getUncopiedTermsIter(); terms.hasNext();) {
                alloy.ast.Node n = (alloy.ast.Node)terms.next();
                n.applyVisitor(new TranslatableASTCheckVisitor());
            }
        }

	/**
	astNode = (alloy.ast.Node) astNode.applyReturnVisitor(new SigmaExprRemover());
	if (!Dbg.userError)
	    astNode.applyVisitor(new TranslatableASTCheckVisitor());
	**/

	//astNode.applyVisitor(new ASTWithSigmaExprsCheckVisitor());
	
	//astNode.applyVisitor(new TranslatableASTCheckVisitor());
	
        return astNode;
    }

    /**
    * Attempt to parse the input string using the specified AlloyParser method
    * @param specString string to parse
    * @param method parser method to use
    * @return a node if parse was successful, otherwise returns null
    **/
    private alloy.ast.Node _parseSpecAs(String specString, int method) {
        // clear previous errors
        Dbg.userError = false;

        // initialize the parser
        final AlloyPrepass.ParserNames parserNames = _sol.getSpecification().getParserNames();
        final StringReader sr = new StringReader(specString);
        //parser.ReInit(sr);
        final AlloyParser parser = new AlloyParser(sr);
        parser.init(parserNames);
        
        alloy.ast.Node astNode = null;
        alloy.parse.syntaxtree.Node cstNode = null;

        try {
            switch (method) {
                case EXPR :
                    cstNode = parser.ExprCST();
                    break;
                case FORMULA :
                    cstNode = parser.FormulaCST();
                    break;
                case INT_EXPR :
                    cstNode = parser.IntExprCST();
                    break;
            }

            // check if the entire string is consumed .. .
            if (sr.read() < 0)
                throw new ParseException("cannot parse entire " + specString + " as " + METHODS[method]);
        } catch (ParseException pe) {
            // Parse exception; set Dbg.userError to true but don't post a message
            Dbg.userError = true;
            _syntaxErr = pe.getMessage();
            return null;
        } catch (alloy.parse.TokenMgrError te) {
            // Parse exception; set Dbg.userError to true but don't post a message
            Dbg.userError = true;
            _syntaxErr = te.getMessage();
            return null;
        } catch (java.io.IOException ioe) {
            // IO Exception from trying to read the next character from the StringReader;
            // if this is the "Stream closed" exception, we are fine since that means that
            // the entire sr stream has been consumed.
            if (ioe.getMessage().indexOf("closed") < 0)
                Dbg.fatal(ioe.getMessage(), ioe);
        }

        // create an AST node from the CST node
        astNode = MakeASTVisitor.getAST(cstNode, _sol.getSpecification());
       
        //    (alloy.ast.Node)cstNode.accept(new MakeASTVisitor(Location.NOT_FROM_FILE, new ArrayList()), null);
	// signal an error if the node is an int cast
	
	astNode.applyVisitor(new IntCastDetectionVisitor());
	if (Dbg.userError)
	    return null;


        // perform semantic checks
        astNode = _performSemanticChecks(astNode);
        if (Dbg.userError)
            return null;

        // perform elaborations
        astNode = _performElaborations(astNode);
        if (Dbg.userError)
            return null;

        //System.out.println("Parsed the string " + specString + " as " + METHODS[method]);
        //System.out.println(astNode.nodeString());
        return astNode;
    }

    /**
     * Evaluates an Alloy expression over a given solution
     * @param specString a String of Alloy (an Expression, Formula, or IntExpression)
     * @return the value of <code>expr</code> evaluated over <code>this._sol</code> or
     * an error message if an error occurred.  Check Dbg.userError to see if a user
     * error occurred.
     **/
    public String evaluate(String specString) {

        // clear previous errors
        _semanticErr = "";
        _syntaxErr = "";
        Dbg.userError = false;

        int parseMethod = 0;

        if (specString == null)
            Dbg.user("attempt to evaluate a null expression");

        if (_sol == null)
            Dbg.user("solution needed for expression evaluation");

        if (Dbg.userError)
            return _semanticErr;

        alloy.ast.Node astNode = null;

        // specString can be an Expression, Formula, or IntExpression
        // so try parsing specString as all of them until one works

        for (int i = 0;(i < NUM_METHODS) && (astNode == null); i++) {
            astNode = _parseSpecAs(specString, i);
            parseMethod = i;
        }
        
        if (astNode == null)
            return ((_semanticErr == "") ? _syntaxErr : _semanticErr);

        TranslVisitor tv = (TranslVisitor)_sol.getTranslator();
        ASTInfoVisitor info = (ASTInfoVisitor)tv.getASTInfoVisitor();

	if (parseMethod == INT_EXPR) {
	    // ExprIntCastExpr -- remove nested SigmaExprs
	    astNode = (alloy.ast.Node) astNode.applyReturnVisitor(new SigmaExprRemover());
	    if (Dbg.userError) return _semanticErr;
	}

        if (parseMethod != EXPR) {
            // ExprIntCastExpr or formula -- we can just call Transl.interpret to get the
            // string output
            astNode.applyVisitor(info);
            //tv.setCaching(false);
            Transl transNode = (Transl)astNode.applyReturnVisitor(tv);
            return transNode.interpret(new PartialAssignment(_sol.getSolution()));
        } else {
            Relation rel = _evaluateExpr((Expr)astNode, false);
            return _relationToString(rel);
        }
    }

    private String _relationToString(Relation rel) {
        //{ (Man_2 Platform_3) (Man_3 Platform_3)  }

        StringBuffer ret = new StringBuffer();

        ret.append("{ ");

        for (Iterator tuples = rel.tuples(); tuples.hasNext();) {
            Tuple tup = (Tuple)tuples.next();

            ret.append("(");

            for (Iterator atoms = tup.atoms(); atoms.hasNext();) {
                Atom atom = (Atom)atoms.next();
                ret.append(atom.toString());
                if (atoms.hasNext()) {
                    ret.append(" ");
                }
            }
            ret.append(") ");

        }

        ret.append("}");

        return ret.toString();
    }


    private Relation _evaluateExpr(Expr astNode, boolean performChecks) {

        if (performChecks) {
            // perform semantic checks
            astNode = (Expr)_performSemanticChecks(astNode);
            if (Dbg.userError)
                return null;

            // perform elaborations
            astNode = (Expr)_performElaborations(astNode);
            if (Dbg.userError)
                return null;
        }

        Relation rel = new Relation();

        TranslVisitor tv = (TranslVisitor)_sol.getTranslator();
        ASTInfoVisitor info = (ASTInfoVisitor)tv.getASTInfoVisitor();

        if (!(astNode instanceof SigmaExpr)) {
            astNode.applyVisitor(info);
            //tv.setCaching(false);
            Transl transNode = (Transl)astNode.applyReturnVisitor(tv);

            ((Instance)_sol)._interpretRelation(
                (ExprTransl)transNode,
                (new PartialAssignment(_sol.getSolution())).toBoolArray(),
                rel);

        } else {
            // evaluate each part separately, and stitch them together
            //List tuples = new ArrayList(); // list of arrays of strings--each array is a tuple
            SigmaExpr sigmaExpr = (SigmaExpr)astNode;
            for (Iterator termsIter = sigmaExpr.getUncopiedTermsIter(); termsIter.hasNext();) {
                Expr term = (Expr)termsIter.next();
                term.applyVisitor(info);
                Transl transNode = (Transl)term.applyReturnVisitor(tv);
                ((Instance)_sol)._interpretRelation(
                    (ExprTransl)transNode,
                    (new PartialAssignment(_sol.getSolution())).toBoolArray(),
                    rel);
            }
        }

        return rel;
    }

    /**
     * returns vizEvaluate(var, cvh, false)
     * 
     * @param var
     * @param cvh
     * @return
     */
    public String vizEvaluate(CustVar var, CustVarHandler cvh) {
        return vizEvaluate(var, cvh, false);
    }
    /**
     * Essentially the same code as evaluate
     *
     * @param validateOnly should be set to true iff you don't want to immediately add the var 
     * and would just like to check validity of the expression
     * @return a null string if there are no errors; otherwise returns the error message 
     */
    public String vizEvaluate(CustVar var, CustVarHandler cvh, boolean validateOnly) {

        String specString = var.getExpr();

        // clear previous errors
        _semanticErr = "";
        _syntaxErr = "";
        Dbg.userError = false;

        if (specString == null)
            Dbg.user("attempt to evaluate a null expression");

        if (_sol == null)
            Dbg.user("solution needed for expression evaluation");

        if (Dbg.userError)
            return _semanticErr;

        alloy.ast.Node astNode = null;

        // only tries to parse as an Expression

        astNode = _parseSpecAs(specString, EXPR);

        if (astNode == null) {
            //System.out.println("syntaxerr: " + _syntaxErr);
            return ((_semanticErr == "") ? _syntaxErr : _semanticErr);
        } else {
            // System.out.println("syntax check passed for " + specString);
        }
        
        if (!validateOnly) {

        TranslVisitor tv = (TranslVisitor)_sol.getTranslator();
        ASTInfoVisitor info = (ASTInfoVisitor)tv.getASTInfoVisitor();

        Relation rel = new Relation();

        if (!(astNode instanceof SigmaExpr)) {
            astNode.applyVisitor(info);
            //tv.setCaching(false);
            Transl transNode = (Transl)astNode.applyReturnVisitor(tv);

            ((Instance)_sol)._interpretRelation(
                (ExprTransl)transNode,
                (new PartialAssignment(_sol.getSolution())).toBoolArray(),
                rel);

        } else {
            // evaluate each part separately, and stitch them together
            List tuples = new ArrayList(); // list of arrays of strings--each array is a tuple
            SigmaExpr sigmaExpr = (SigmaExpr)astNode;

            for (Iterator termsIter = sigmaExpr.getUncopiedTermsIter(); termsIter.hasNext();) {
                Expr term = (Expr)termsIter.next();
                term.applyVisitor(info);
                Transl transNode = (Transl)term.applyReturnVisitor(tv);
                ((Instance)_sol)._interpretRelation(
                    (ExprTransl)transNode,
                    (new PartialAssignment(_sol.getSolution())).toBoolArray(),
                    rel);
            }

        }

        // list of AlloySet's (or AlloyRelation's) corrseponding to the
        // partitioned (if application) parts of the cust var
        List eltList = new ArrayList();

        // list of List of AlloyAtom's, each corresponding to the instance
        // of the corresponding set or rel in eltList
        List atomLists = new ArrayList();

        for (Iterator typeIter = ((Expr)astNode).getType().getTypeIter(); typeIter.hasNext();) {

            RelationType relType = (RelationType)typeIter.next();

            if (relType.arity() == 1) {
                // a set
                SigType setType = (SigType)relType.getBasicTypeAt(0);

                AlloyType alyType =
                    (AlloyType) ((Set)((Instance)_sol).getVizElt(setType.getSignature().getLeafId())).iterator().next();

                // create the AlloySet
                String setName = var.getName();
                // this case is for unary skolems, which are VariableExprs
                AlloySet alySet = new AlloySet(setName, alyType);
                eltList.add(alySet);

            } else {
                // A Relation
                List alyTypes = new ArrayList();
                for (Iterator typesIter = relType.getTypeIter(); typesIter.hasNext();) {
                    SigType curType = (SigType)typesIter.next();

                    AlloyType alyType =
                    (AlloyType) ((Set)((Instance)_sol).getVizElt(curType.getSignature().getLeafId())).iterator().next();
                    // add to the List of types
                    alyTypes.add(alyType);

                }
                // create the AlloyRelation
                String relName = var.getName();
                AlloyRelation alyRel = new AlloyRelation(relName, alyTypes);
                eltList.add(alyRel);
            }

        }

        // initialize each elt of atomLists to a List
        for (int i = 0; i < eltList.size(); i++) {
            atomLists.add(new ArrayList());
        }

        Object vizElt = eltList.get(0);
        if (vizElt instanceof AlloySet) {
            // a set
            for (Iterator tupIter = rel.tuples(); tupIter.hasNext();) {
                Tuple tup = (Tuple)tupIter.next();
                Iterator atomIter = tup.atoms();
                Atom atom = (Atom)atomIter.next();
                Dbg.chk(!atomIter.hasNext());
                // should not have any more atoms, since set is unary
                AlloyAtom alyAtom = ((Instance)_sol).getAlloyAtom(atom);
                Dbg.chk(alyAtom);

                // if this set got partitioned, determine to which atom this
                // atom belongs.  if the set didn't get partitioned, add to
                // first AlloySet in eltSet w/o checking
                if (eltList.size() == 1) {
                    ((List)atomLists.get(0)).add(alyAtom);
                } else {

                    AlloyType atomType = alyAtom.getType();
                    int counter = 0;
                    for (Iterator eltIter = eltList.iterator(); eltIter.hasNext();) {
                        AlloySet curSet = (AlloySet)eltIter.next();
                        AlloyType curSetType = curSet.getType();

                        if (isSubtypeOf(atomType, curSetType)) {
                            ((List)atomLists.get(counter)).add(alyAtom);
                            break;
                        }

                        counter++;
                    }
                }
            }
        } else {
            // a relation
            for (Iterator tupIter = rel.tuples(); tupIter.hasNext();) {
                Tuple tup = (Tuple)tupIter.next();
                List alyAtoms = new ArrayList();

                Iterator atomIter = tup.atoms();
                while (atomIter.hasNext()) {
                    Atom atom = (Atom)atomIter.next();
                    AlloyAtom alyAtom = ((Instance)_sol).getAlloyAtom(atom);
                    Dbg.chk(alyAtom);
                    alyAtoms.add(alyAtom);
                }
                AlloyTuple alyTup = new AlloyTuple(alyAtoms);

                if (eltList.size() == 1) {
                    ((List)atomLists.get(0)).add(alyTup);
                } else {
                    // relation got partitioned, so we need to determine to which partitioned
                    // part this tuple belongs.

                    // note: there's some amount of arbituaryness in this
                    // scheme.  suppose foo has type (A->B1->C) + (A->B->C1).
                    // Then the a tuple like (A_1, B1_1, C1_1) can belong to both.

                    int counter=0;
                    for (Iterator eltIter = eltList.iterator(); eltIter.hasNext();) {
                        AlloyRelation curRel = (AlloyRelation)eltIter.next();
                        boolean tupleOk = true;

                        Iterator tupAtomIter = alyTup.getAtoms().iterator();
                        for (Iterator relTypeIter = curRel.getTypes().iterator(); relTypeIter.hasNext();) {
                            AlloyType curRelType = (AlloyType)relTypeIter.next();
                            AlloyAtom curAtom = (AlloyAtom)tupAtomIter.next();
                            AlloyType curAtomType = curAtom.getType();
                            if (!isSubtypeOf(curAtomType, curRelType)) {
                                // failed
                                tupleOk = false;
                                break;
                            }
                        }

                        if (tupleOk) {
                            ((List)atomLists.get(counter)).add(alyTup);
                            break;
                        }

                        counter++;

                    }
                }

            }
        }

        cvh.processAtoms(var, eltList, atomLists);
        }

        return null;
    }

    private boolean isSubtypeOf(AlloyType subType, AlloyType superType) {
        boolean hit = false;

        while (superType != null) {
            if (superType.equals(subType)) {
                hit = true;
                break;
            }
            superType = ((Instance)_sol).getVizInstance().getSuperForType(superType);
        }

        return hit;
    }

    private String _makeTupleString(List tuples) {
        String s = "{ ";
        for (Iterator tupleIter = tuples.iterator(); tupleIter.hasNext();) {
            String[] atoms = (String[])tupleIter.next();
            s += "(";
            for (int i = 0; i < atoms.length; i++) {
                s += ((atoms[i]) + (i == atoms.length - 1 ? "" : " "));
            }
            s += ") ";
        }
        return s += " }";
    }

    private List _toTupleList(String valString_, int tupleSize_) {
        Dbg.chk(tupleSize_ > 0);
        // skip "{ " in value string
        int index = 2;
        List tupleList = new ArrayList();
        while (valString_.charAt(index) == '(') {
            index++;
            String[] curTuple = new String[tupleSize_];
            for (int i = 0; i < tupleSize_; i++) {
                int atomEnd =
                    (i == tupleSize_ - 1) ? valString_.indexOf(')', index) : valString_.indexOf(' ', index);
                curTuple[i] = valString_.substring(index, atomEnd);
                index = atomEnd + 1;
            }
            tupleList.add(curTuple);
            index++;
        }
        return tupleList;
    }

    public void debugMsg(int msgType_, String msg_, Throwable thrown_) {
        int fileInfo = msg_.indexOf(NO_FILE_INFO);
        if (fileInfo < 0)
            _semanticErr = msg_;
        else
            _semanticErr =
                msg_.substring(0, fileInfo) +
                msg_.substring(fileInfo + NO_FILE_INFO.length(), msg_.length());

    }

    public void debugMsg(int msgType_, Msg msg_, Throwable thrown_) {
        debugMsg(msgType_, msg_.toString(), thrown_);
    }

    public static void main(String[] args) {
        if (args.length < 3)
            System.out.println("usage:  java alloy.api.AlloyEvaluator [model] [command] [expression]");
        else {
            Dbg.DbgMsgListener msgListener = new Dbg.DbgMsgStreamPrinter(System.out);
            Dbg.addDbgMsgListener(Dbg.USER, Dbg.INFO, msgListener);
            Dbg.addDbgMsgListener(
                Dbg.WARN,
                Dbg.FATAL,
                Dbg.UNIMPL,
                new Dbg.DbgMsgStreamPrinter(System.out, Dbg.STACK_FULL));
            if (AlloyRunner.prepareSpec(args[0])) {
                alloy.ast.Commands coms = AlloyRunner.getCommands();
                if (coms == null) {
                    System.out.println("No commands available");
                    return;
                }
                java.util.Iterator cIter = coms.getCommandIter();
                alloy.ast.FindCommand com;
                while (cIter.hasNext()) {
                    com = (alloy.ast.FindCommand)cIter.next();

                    if (com.toString().indexOf(args[1]) >= 0) {
                        System.out.println(com.toString());
                        try {
                            long seed = 0;
                            SolutionData sd =
                                AlloyRunner.analyzeCommand(AlloyRunner.translateCommand(com), seed);
                            AlloyEvaluator ae = new AlloyEvaluator(sd);
                            Dbg.removeDbgMsgListener(Dbg.USER, msgListener);
                            String sol = ae.evaluate(args[2]);
                            Dbg.addDbgMsgListener(Dbg.USER, msgListener);
                            System.out.println(sol);
                        } catch (Exception e) {
                            Dbg.fatal(e.getMessage());
                        }
                        return;
                    }
                }
                System.out.println("Couldn't find the command " + args[1] + " in " + args[0]);
            }
        }
    }
    
    private static final class IntCastDetectionVisitor extends ASTDepthFirstVisitor {

	public void visit(IntExprCastExpr expr_) {
	    Dbg.user(new Msg("cannot evaluate an integer cast",expr_));
	}

    }


    /** Removes SigmaExprs from an AST node **/
    private static final class SigmaExprRemover extends ASTDepthFirstReplacer {

	public Object visit(SigmaExpr sigmaExpr_) {
	    if (sigmaExpr_.numChildren() != 1) {
		Dbg.user(new Msg("cannot atomize the expression",sigmaExpr_));
		return sigmaExpr_;
	    } else {
                return sigmaExpr_.getUncopiedTermsIter().next();
            }
	}
    }


    /**
     */
    public void cleanup() {
        Dbg.removeDbgMsgListener(this);
        
    }

}
